\begin{tabbing}
$\forall$$T$:Type, $E$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]EquivRel($T$;$x$,$y$.$E$($x$,$y$))
\\[0ex]$\Rightarrow$ \=($\forall$$F$:(($x$,$y$:$T$//$E$($x$,$y$))$\rightarrow\mathbb{P}$).\+
\\[0ex]($\forall$$w$:($x$,$y$:$T$//$E$($x$,$y$)). SqStable($F$($w$))) $\Rightarrow$ (($\forall$$z$:($x$,$y$:$T$//$E$($x$,$y$)). $F$($z$)) $\Leftarrow\!\Rightarrow$ ($\forall$$z$:$T$. $F$($z$))))
\-
\end{tabbing}